(*
** Implementacion de los tipos y operaciones definidas en Lang.v.
*)

Require Export ZArith.
Require Import Matrix.
Require Import Lang.


Module TypesImpl <: Types.

Definition Bool := bool.
Definition Integer := Z.
Definition Byte := Z.
Definition Matrix A m n := Matrix.Matrix A (Z.to_nat m) (Z.to_nat n).
Definition TRUE := true.
Definition FALSE := false.
Definition ZERO := 0%Z.
Definition int_plus := Z.add.
Definition ONE := 1%Z.
Definition bool_not := negb.
Definition bool_and := andb.
Definition bool_or := orb.
Definition int_minus := Z.sub.
Definition int_mult := Z.mul.
Definition int_div := Z.div.
Definition int_modulo := Z.modulo.
Definition int_eq := Z.eqb.
Definition int_lt := Z.ltb.
Definition int_le := Z.leb.
Definition byte_gt := Z.gtb.
Definition int_gt := Z.gtb.
Definition byte_eq := Z.eqb.
Definition int_ge := Z.geb.
Definition byte_xor := Z.lxor.
Definition byte_shl := Z.shiftl.
Definition byte_shr := Z.shiftr.
Definition matrix_get A m n i j (matr: Matrix A m n) := Matrix.get (Z.to_nat i) (Z.to_nat j) matr.
Definition matrix_set A m n (matr: Matrix A m n) i j a := Matrix.set (Z.to_nat i) (Z.to_nat j) a matr.
Definition byte_and := Z.land.
Definition matrix_zero (A:Set) (a:A) m n := Matrix.new_matr a (Z.to_nat m) (Z.to_nat n).

Definition z_to_integer(z: Z): Integer := z.
Coercion z_to_integer : Z >-> Integer.

Definition bool_to_Bool(b: bool): Bool := b.
Coercion bool_to_Bool : bool >-> Bool.

Definition z_to_byte (z:Z) : Byte := z.
Coercion z_to_byte : Z >-> Byte.

End TypesImpl.


Module LangImpl := Lang.Lang TypesImpl.
Export TypesImpl.
Export LangImpl.
